import {drop, pipe, reduce, reverse} from './iterator.js'
import {Formula} from './formula.js'
import {type FreeVariableTerm, QuantifiedVariableTerm} from './term.js'
import {identity} from './functional.js'

function unifiable(formula1: Formula, formula2: Formula) {
    return formula1.unify(formula2, new Map, new Map)
}

type ThesisItem =
    | {type: 'let' | 'given' | 'take', variable: FreeVariableTerm}
    | {type: 'assume' | 'thus', formula: Formula}

export class Reasoner {
    thesis: Formula | undefined
    thesisItems: ThesisItem[] = []

    constructor(thesis?: Formula) {
        this.thesis = thesis
    }

    checkLet(variable: FreeVariableTerm) {
        this.thesisItems.push({type: 'let', variable})

        if (this.thesis)
            if (
                this.thesis instanceof Formula.Generalization &&
                this.thesis.variable.getType() === variable.getType()
            )
                this.thesis = this.thesis.operand.substitute(new Map([[this.thesis.variable, variable]]))
            else
                return false

        return true
    }

    checkGiven(variable: FreeVariableTerm) {
        this.thesisItems.push({type: 'given', variable})

        if (!this.thesis)
            return true

        if (!(this.thesis instanceof Formula.Implication))
            return false

        const [antecedent, consequent] = this.thesis.operands

        if (antecedent instanceof Formula.Existence && antecedent.variable.getType() === variable.getType())
            this.thesis = new Formula.Implication([antecedent.operand, consequent])
                .substitute(new Map([[antecedent.variable, variable]]))
        else
            return false

        return true
    }

    checkTake(variable: FreeVariableTerm) {
        this.thesisItems.push({type: 'take', variable})

        if (!this.thesis)
            return true

        if (!(this.thesis instanceof Formula.Existence))
            return false

        this.thesis = this.thesis.operand.substitute(new Map([[this.thesis.variable, variable]]))

        return true
    }

    checkAssume(formula: Formula) {
        this.thesisItems.push({type: 'assume', formula})

        return this.checkDirectAssume(formula) || this.checkIndirectAssume(formula)
    }

    checkDirectAssume(formula: Formula) {
        if (!this.thesis)
            return true

        if (!(this.thesis instanceof Formula.Implication))
            return false

        const [antecedent, consequent] = this.thesis.operands

        if (unifiable(antecedent, formula))
            this.thesis = consequent
        else if (antecedent instanceof Formula.Conjunction && unifiable(antecedent.operands[0], formula))
            this.thesis = new Formula.Implication([antecedent.operands[1], consequent])
        else
            return false

        return true
    }

    checkIndirectAssume(formula: Formula) {
        if (!this.thesis)
            return true

        if (formula instanceof Formula.Implication &&
            formula.operands[1] == Formula.False &&
            unifiable(formula.operands[0], this.thesis)
        ) {
            this.thesis = Formula.False
            return true
        }

        return false
    }

    checkThus(formula: Formula) {
        this.thesisItems.push({type: 'thus', formula})

        if (this.thesis)
            if (unifiable(this.thesis, formula))
                this.thesis = Formula.True
            else if (this.thesis instanceof Formula.Conjunction && unifiable(this.thesis.operands[0], formula))
                [, this.thesis] = this.thesis.operands
            else
                return false

        return true
    }

    getReasoningThesis() {
        const lastItem = this.thesisItems.at(-1)
        const shouldSkip = lastItem?.type == 'thus'

        return pipe(
            this.thesisItems,
            reverse,
            shouldSkip ? drop(1) : identity,
            reduce(
                (thesis, thesisItem) => {
                    switch (thesisItem.type) {
                    case 'assume':
                        return new Formula.Implication([thesisItem.formula, thesis])

                    case 'given': {
                        const {variable} = thesisItem

                        const implicationThesis = thesis instanceof Formula.Implication
                            ? thesis
                            : new Formula.Implication([Formula.True, thesis])

                        return new Formula.Implication([
                            new Formula.Existence(variable, implicationThesis.operands[0]),
                            implicationThesis.operands[1],
                        ])
                            .substitute(new Map([[variable, new QuantifiedVariableTerm(variable)]]))
                    }

                    case 'let': {
                        const {variable} = thesisItem

                        return new Formula.Generalization(variable, thesis)
                            .substitute(new Map([[variable, new QuantifiedVariableTerm(variable)]]))
                    }

                    case 'take': {
                        const {variable} = thesisItem

                        return new Formula.Existence(variable, thesis)
                            .substitute(new Map([[variable, new QuantifiedVariableTerm(variable)]]))
                    }

                    case 'thus':
                        return new Formula.Conjunction([thesisItem.formula, thesis])
                    }
                },
                shouldSkip ? lastItem.formula : Formula.True,
            ),
        )
    }
}
